\begin{tabbing}
$\vdash$  \=$\forall$$S$,$T$:Type, $P$,$Q$:($S$$\rightarrow\mathbb{P}$).\+
\\[0ex]($S$ = $T$) $\Rightarrow$ ($\forall$$x$:$S$. $P$($x$) $\Leftarrow\!\Rightarrow$ $Q$($x$)) $\Rightarrow$ (($\exists$$x$:$S$. $P$($x$)) $\Leftarrow\!\Rightarrow$ ($\exists$$y$:$T$. $Q$($y$)))
\-
\end{tabbing}